(* Copyright Per Lindgren 2015, see the file "LICENSE" *)
(* for the full license governing this code.           *)

(* FUN-4SURE/WhyML *)

open Common
open Options
open AST
open ST
open Env
open List


let why_of_bo = function
  | true  -> "true"
  | false -> "false" 

type env_t =
  | In
  | Out
  | Local
  | Temp

let env_of_v l_env id =
  let (ivl, ovl, lvl, tvl) = l_env in
  
  match (mem id ivl, mem id ovl, mem id lvl, mem id tvl) with
  | (true, _, _, _) -> In
  | (_, true, _, _) -> Out
  | (_, _, true, _) -> Local
  | (_, _, _, true) -> Temp 
  | _              -> raise (RtfmError("Internal error, identifier not in envirnment!"))

let pre_sid sid = match sid with
  | "" -> ""
  | _  -> "_" ^ sid
  
let pre_of_env sid = function
  | In    -> "iv"
  | Out   -> "v.ov" ^ pre_sid sid
  | Local -> "v.lv" ^ pre_sid sid
  | Temp  -> "v.tv" ^ pre_sid sid
  
let post_of_env sid id = function 
  | In
  | Out
  | Local -> ""
  | Temp  -> sid ^ "_" 

let why_of_id exp_env id = 
  let l_env, sid, is_pred = exp_env in
  let env = env_of_v l_env id in
  
  let old t = match is_pred with
  | true  -> "old (" ^ t ^ ")"
  | false -> t
  in
  
  old (pre_of_env sid env ^ "." ^ post_of_env sid id env ^ st_of_id id)
  
let rec why_of_op exp_env = function
  | OpAnd  -> "&&"
  | OpOr   -> "||"
  | OpExor -> "" (* not sure if this is correct *)
  | OpMul  -> "*"
  | OpDiv  -> "/"
  | OpMod  -> "%"
  | OpAdd  -> "+"
  | OpSub  -> "-"
  | OpEq   -> "="
  | OpNeq  -> "<>"
  | OpGt   -> ">"
  | OpGEq  -> ">="
  | OpLt   -> "<"
  | OpLEq  -> "<="
and why_of_uop = function
  | UNot   -> "!"
  | UMinus -> "-"
and why_of_exp exp_env = function
  | OpExp (op, e1, e2) -> "(" ^ why_of_exp exp_env e1 ^ " " ^ why_of_op exp_env op ^ " " ^ why_of_exp exp_env e2 ^ ")"
  | IdExp (id)         -> why_of_id exp_env id 
  | IntExp (i)         -> string_of_int i
  | CharExp (c)        -> ecit ^ String.make 1 c ^ ecit
  | BoolExp (b)        -> why_of_bo b
  | UnOpExp (uop, e)   -> "(" ^ why_of_uop uop ^ "(" ^ why_of_exp exp_env e ^ "))"

(*
let why_of_st_stmt l_env = function
  | StmtAssign (lid, exp) -> "  " ^ why_of_id l_env false lid  ^ " <- " ^ why_of_exp l_env false exp 
  | StmtAssert (exp)      -> "  assert { " ^ why_of_exp l_env false exp ^ " }" (* PER to fix *)
*)

(*  
let why_of_gu_exp exp = 
  "[ " ^ why_of_exp ([],[],[], []) false exp ^ " ]"  
        
let why_of_gu = function
  | EcGuard (Some t, _, _)     -> "AFTER " ^ string_of_int t 
  | EcGuard (_, None, exp)     -> why_of_gu_exp exp
  | EcGuard (_, Some evt, exp) -> st_of_id evt ^ " " ^ why_of_gu_exp exp
  
let why_of_tr tl = 
  let tr = function
    | EcTrans (f,t,g) -> "  " ^ st_of_id f ^ " TO " ^ st_of_id t ^ " := " ^ why_of_gu g ^ ";"
    in
    myconcat nl (List.map tr tl)

let why_of_action = function
  | EcAction (Some aid, eidl) -> st_of_id aid ^ " -> " ^ String.concat ", " (List.map st_of_id eidl)
  | EcAction (None, eidl)     -> " -> " ^ String.concat ", " (List.map st_of_id eidl)
    
let why_of_sl sl =
  let st = function
    | EcState (sid, al) -> " " ^ st_of_id sid ^ " : " ^ String.concat ", " (List.map why_of_action al) ^ ";"
  in   
  myconcat nl (List.map st sl)
*)

let why_of_ptype = function
  | Int  -> "int"
  | Bool -> "bool"
  | Char -> "char"
  | Byte -> "byte"
   
let why_of_event id =
  "Ev_" ^ st_of_id id  

let rec why_of_eventl = function
  | []     -> "Nil"
  | e :: l -> why_of_event e  ^ " :: (" ^ why_of_eventl l ^ ")" 
      
          
let why_of_var = function
  | Var (id, t) -> st_of_id id ^ " : " ^ why_of_ptype t 
  
let why_of_sid sid = 
  "S_" ^ st_of_id sid  

(* let remove v vl = filter (fun v' -> v <> v') vl
*)
let why_of_fb fb_if fb_v fb_ecc fb_algl = 
   
  (* variables *)
  let ivl   = vil_of_if fb_if in 
  let ovl   = vol_of_if fb_if in
  let lvl   = vl_of_v fb_v in
  (*let l_env = (ivl, ovl, lvl) in*)
  
  (* events *)
  let eil    = eil_of_if fb_if in 
  let ei_idl = map id_of_e eil in
  
  let eol    = eol_of_if fb_if in
  let oe_idl = map id_of_e eol in
    
  (* interface variable types *) 
  let var_t_of =
    
    (* variables *)
    let of_v v = "  " ^ why_of_var v  in 
     
    "(* input variables    *)" ^ nl ^
    "type i_var_t = {" ^ nl ^
       myconcat (";" ^ nl) (map of_v ivl) ^
       (if ivl = [] then "  i_var_dummy : ()" else "") ^ nl ^ 
    "}" ^ nl ^ nl ^ 
    (
    if ovl <> [] then
    "(* output variables   *)" ^ nl ^
    "type o_var_t = {" ^ nl ^
    myconcat (";" ^ nl) (map of_v ovl) ^ 
    "}" ^ nl ^ nl
    else ""
    ) ^
    (
    if lvl <> [] then
    "(* local (internal) variables *)" ^ nl ^
    "type l_var_t = {" ^ nl ^
    myconcat (";" ^ nl) (map of_v lvl) ^   
    "}" ^ nl ^ nl
    else ""
    ) ^ 
    
    "(* state variables *)" ^ nl ^ 
    "type var_t = { " ^ nl ^ 
    (if ovl <> [] then "  ov : o_var_t;" ^ nl else "" ) ^  
    (if lvl <> [] then "  lv : l_var_t;" ^ nl else "" ) ^ 
    (if ovl = [] && lvl = [] then "  var_dummy : ()" ^ nl else "") ^   
    "}" ^ nl ^ nl 
    
  in
  
  (* interface event types *)
  let event_t_of =
    
    let of_e e = "  | " ^ why_of_event e  in 
    "(* events *)" ^ nl ^ 
    "type event_t = " ^ nl ^
    "  (* input events    *)" ^ nl ^
    myconcat (nl) (map of_e ei_idl) ^ nl ^
    "  (* output events   *)" ^ nl ^
    myconcat (nl) (map of_e oe_idl) ^ nl
  in  
  
  (* interface state types *)
  let ecc_t_of = 
    match fb_ecc with
    | None -> "" (* if no ECC  skip *)
    | Some FbEcc (sl, _, tl) -> 
      let why_s_of = function
        | EcState (sid, _) -> "  | " ^ why_of_sid sid
      in
      "(* ECC states *)" ^ nl ^ 
      "type ecc_t = " ^ nl ^
      myconcat (nl) (map why_s_of sl) ^ nl 
  in
   
  let why_of_algs  =
    
    let ver_of_alg = function
      | FbAlg (aid, cont, tvl, stmtl) -> 
        
        let sid = st_of_id aid in
        
        "(* algorithm " ^ sid ^ " *)" ^ nl ^ nl ^ 
        
        ( 
          if opt.verbose then "(* " ^ nl ^ st_of_alg (FbAlg (aid, cont, tvl, stmtl)) ^ nl ^ "*)" ^ nl ^ nl 
          else "" 
        ) ^ 
        
        (* generate temporary variable container *)
        (
        if tvl <> [] then
        "type t_var_" ^ sid ^ "_t = { " ^ nl ^ 
        let of_v v = "  " ^ sid ^ "_" ^ why_of_var v  in 
        myconcat (";" ^ nl) (map of_v tvl) ^ 
        "}" ^ nl ^ nl 
        else ""
        ) ^ 
        
        (* generate algorithm state *)
        "type v_" ^ sid ^ "_t = { " ^ nl ^
        (if ovl <> [] then "  ov_" ^ sid ^ " : o_var_t;" ^ nl  else "") ^ 
        (if lvl <> [] then "  lv_" ^ sid ^ " : l_var_t;" ^ nl  else "") ^ 
        (if tvl <> [] then "  tv_" ^ sid ^ " : t_var_"^ sid ^ "_t;" ^ nl  else "") ^ 
        "}" ^ nl ^ nl ^
        
        (* generate algorithm statement functions *)
        
        let v_env = (map id_of_va ivl, map id_of_va ovl, map id_of_va lvl, map id_of_va tvl) in
        (* let pre_of_v = pre_of_env sid v_env in *)
        
        let with_of_env = function 
        | In    -> raise (RtfmError("Internal error, should update input variables!"))
        | Out   -> "ov_" ^ sid
        | Local -> "lv_" ^ sid
        | Temp  -> "tv_" ^ sid
        in
        
        let with2_of_env = function 
        | In    -> raise (RtfmError("Internal error, should update input variables!"))
        | Out    
        | Local -> "" 
        | Temp  -> sid ^ "_"
        in
        
        let f_alg_stmt i = function 
          | StmtAssign (lid, exp) -> 
            ( 
              if opt.verbose then 
                "(* " ^ sid ^ "_st" ^ i ^ " : " ^ st_of_st_stmt (StmtAssign (lid, exp)) ^ " *)" ^ nl 
              else "" 
            ) ^
            let env = env_of_v v_env lid in
            "function f_" ^ sid ^ "_st" ^ i ^ " (iv : i_var_t) (v : v_" ^ sid ^ "_t) : v_" ^ sid ^ "_t  = " ^ nl ^
            "  { v with " ^ with_of_env env ^ " = { v." ^ with_of_env env ^ 
            " with " ^ with2_of_env env ^ st_of_id lid ^ " = " ^ 
            why_of_exp (v_env, sid, false) exp ^ "}; }" ^ nl
         (*    "  f_assign_" ^ st_of_id lid  ^ " " ^ why_of_exp ([],[],[]) false exp *)
          | StmtAssert (exp)      -> "  NOT IMPLEMENTED " (* PER to fix *)
        in
        
        let to_index l = 
          let rec aux i = function
          | []     -> []
          | _ :: l -> i :: (aux (i+1) l )
          in
          aux 1 l
        in
        let st_il = map string_of_int (to_index stmtl) in
        let st_stmtl = map2 f_alg_stmt st_il stmtl in
           
        myconcat nl st_stmtl ^ 
        
        (* generate algorithm function *)
        
        let rec f_alg = function
          | []         -> raise (RtfmError("Internal error, should have at least one statement!"))
          | st_i :: [] -> "f_" ^ sid ^ "_st" ^ st_i ^ " iv v" 
          | st_i :: il -> "f_" ^ sid ^ "_st" ^ st_i ^ " iv " ^ "(" ^ f_alg il ^ ")"
        in
        
        let of_ptype_v = function
          | Bool -> "false"
          | Int  -> "0"
          | _    -> raise (RtfmError("Internal error, ptype not supported!"))
        in
        
        let of_tv tv = sid ^ "_" ^ st_of_id (id_of_va tv) ^ " = " ^ of_ptype_v (t_of_va tv) in
        
        "function f_" ^ sid ^ " (iv : i_var_t) (v : var_t) : var_t  = " ^ nl ^
        "  let v = { " ^
        (if ovl <> [] then "ov_" ^ sid ^  " = v.ov; " else "") ^ 
        (if lvl <> [] then "lv_" ^ sid ^  " = v.lv; " else "") ^ 
        (if tvl <> [] then 
          "tv_" ^ sid ^ " = { " ^ myconcat "; " (map of_tv tvl) ^ "}; " 
          else "") ^ "} in " ^ nl ^
        "  let v = " ^ f_alg (rev st_il) ^ " in" ^ nl ^ 
        "  { " ^ 
        (if ovl <> [] then "ov = v.ov_" ^ sid ^ "; " else "") ^ 
        (if lvl <> [] then "lv = v.lv_" ^ sid ^ "; " else "") ^ 
        "}" ^ nl ^ nl         
    in 
    
    "(* algorithm verification *)" ^ nl ^ 
    myconcat nl (map ver_of_alg fb_algl) ^ nl  
  in
      
  let why_of_ecc = 
    match fb_ecc with
    | None -> "" (* if no ECC  skip *)
    | Some FbEcc (sl, _, _) ->
      
      let rec f_of = function
        | []       -> "v"
        | id :: [] -> "f_" ^ st_of_id id ^ " iv v" 
        | id :: l  -> "f_" ^ st_of_id id ^ " iv (" ^ f_of l ^ ")" 
      in  
      let f_alg_of = function
        | EcState (sid, al) ->
          "(* entry actions for state " ^ st_of_id sid ^ " *)" ^ nl ^ 
          "function f_v_" ^ st_of_id sid ^ " (iv : i_var_t) (v : var_t) : var_t = " ^ nl ^
          "  " ^ f_of (rev (filt_opt aid_of_act al)) ^ nl ^ nl ^ 
          "val v_" ^ st_of_id sid ^ " (iv : i_var_t) (v : var_t) : var_t " ^ nl ^
          "  ensures { result = " ^ "f_v_" ^ st_of_id sid ^ " iv  v }" ^ nl 
      in
      
      "(* actions *) " ^ nl ^ nl ^
      myconcat nl (map f_alg_of sl) ^ nl ^ 
      
      let rec cons = function
        | []     -> "Nil"
        | e :: l -> why_of_event e  ^ " :: (" ^ cons l ^ ")" 
      in
       
      let f_event_of = function
        | EcState (sid, al) ->
          "(* entry events for state " ^ st_of_id sid ^ " *)" ^ nl ^ 
          "constant c_e_" ^ st_of_id sid ^ " : list event_t = " ^ nl ^
          "  " ^ cons (concat (map eid_of_act al)) ^ nl
      in
      
      myconcat nl (map f_event_of sl) ^ nl  
  in

  
  let why_of_ecc_ex = 
    match fb_ecc with
    | None                    -> ""
    | Some FbEcc (sl, cl, trl) ->

    (* let of_ecc 
    let of_state = function
      | EcState (sid, actl) ->
        "  | (" ^ why_of_sid sid ^ ", _) -> (f_v_" ^ st_of_id sid ^ " iv v, c_e_" ^ st_of_id sid ^ ")"   
    in      
    *)
    let v_env = (map id_of_va ivl, map id_of_va ovl, map id_of_va lvl, []) in 

    let of_trans = function
      | EcTrans (s_sid, d_sid, EcGuard (_, eido, expr)) ->
        "  | (" ^ why_of_sid s_sid ^ ", " ^ 
        (
          match eido with
          | None -> "None"
          | Some eid -> "Some " ^ why_of_event eid 
        ) ^ 
        
        ") -> " ^ nl ^ 
        let e = "Some (" ^ why_of_sid d_sid ^ ", v_" ^ st_of_id d_sid ^ " iv v, c_e_" ^ st_of_id d_sid ^ ")" in
        match expr with
        | BoolExp true -> "    " ^ e
        | _            -> "    if " ^ why_of_exp (v_env, "", false) expr ^ " then " ^ e ^ " else None"   
    in        
    
    let why_of_contract = function 
    (*
      | Requires expr  -> "  requires { " ^ why_of_exp l_var false expr ^ " }"  (* PER to fix *)     
      | Ensures  expr  -> "  ensures  { " ^ why_of_exp l_var false expr ^ " }" 
     *)
      | ReqRaw   s     -> "  requires " ^ s       
      | EnsRaw   s     -> "  ensures  " ^ s

    in
      
    "(* ECC action execution *)" ^ nl ^ nl ^ 
    "type ecc_ex_t = (ecc_t, var_t, list event_t)" ^ nl ^ nl ^
    "let rec f_ecc_ex" ^ nl ^
    "  (s : ecc_t)" ^ nl ^
    "  (e : option event_t)" ^ nl ^ 
    "  (iv : i_var_t)" ^ nl ^
    "  (v : var_t)" ^ nl ^
 (*   "  (el : list event_t)" ^ nl ^ *)
    "  (l : list ecc_t)" ^ nl ^
    "  : ecc_ex_t" ^ nl ^
    nl ^
    "  variant { length l }" ^ nl ^ 
    "  requires { mem s l }" ^ nl ^  
    myconcat nl (map why_of_contract cl) ^ 
  
    "= " ^ nl ^
    (*"  let (n : option ecc_ex_t) = match s, e with " ^ nl ^*)
    "  let n = match s, e with " ^ nl ^
    myconcat (nl ^ nl) (map of_trans trl) ^ 
    "  | (_, _) -> " ^ nl ^
    "    None" ^ nl ^
    "  end in" ^ nl ^
    nl ^
    "  match n with" ^ nl ^
    "  | None -> (s, v, Nil)" ^ nl ^
    "  | Some (s', v', el') ->"  ^ nl ^
    "    match mem s' l with" ^ nl ^
    "    | False -> (s, v, Nil)" ^ nl ^
    "    | True  -> " ^ nl ^
    "      let l' = remove s l in" ^ nl ^
    "      let (s, v, el) = f_ecc_ex s' None iv v' l' in (s, v, el' ++ el)" ^ nl ^ 
    "    end" ^ nl ^
    "  end" ^ nl ^ nl
    
  in     
  
  (* interface *)
  var_t_of ^       (* variables       *)
  event_t_of ^     (* type event_t    *)
  ecc_t_of ^       (* ecc states      *)
  
  (* algorithms *)
  why_of_algs ^    (* algorithms      *)
  why_of_ecc ^     (* ecc actions     *)  
  why_of_ecc_ex ^ 
  (*
  
  ecc_t_of ^       (* type ecc_t      *)
  fb_state_t_of ^  (* type fb_state_t *)
  *)
  ""


    (*
    let fb_state_t_of =
    let vil    = vil_of_if fb_if in 
    let vol    = vol_of_if fb_if in
    let vl     = vl_of_v fb_v in
    
    let has_var = if concat [vil; vol; vl] <> [] then
      "            v : var_t;" ^ nl else "" in
      
    match fb_ecc with 
    | Some FbEcc (EcState (s, _) :: _, _, _) ->
      
      "type fb_state_t = {" ^ nl ^ 
      "  mutable ecc : ecc_t;" ^ nl ^
      has_var ^
      "}" ^ nl ^ nl ^
      "val mk_fb_state () : fb_state_t " ^ nl ^ 
      "  ensures { " ^ nl ^
      "    result.ecc = " ^ why_of_sid s ^ " /\\" ^ nl ^  
      "    true (* result.v   = not yet implemented *)" ^ nl ^  
      "  } " ^ nl ^ nl 
    | _ ->
      "(* no ECC *)" ^ nl  
    *)
 

(*
let of_ptype_v = function
  | Bool -> "false"
  | Int  -> "0"
  | _    -> raise (RtfmError("Internal error, ptype not supported!"))
    
let ref_of_var = function
  | Var (id, t) -> "  let " ^ st_of_id id ^ " = ref " ^ of_ptype_v t 

let ref_of_vars vl =
  myconcat (" in" ^ nl) (List.map ref_of_var vl) 

let why_of_stmts l_env stmtl = 
  String.concat (";" ^ nl) (List.map (why_of_st_stmt l_env) stmtl) 
    
let why_of_contract l_var cl = 
  let of_contract = function
    | Requires expr  -> "  requires { " ^ why_of_exp l_var false expr ^ " }"  (* PER to fix *)     
    | Ensures  expr  -> "  ensures  { " ^ why_of_exp l_var false expr ^ " }" 
    | ReqRaw   s     -> "  requires " ^ s       
    | EnsRaw   s     -> "  ensures  " ^ s
  in
  myconcat nl (List.map of_contract cl)
*)

(*
let pred_of_st_stmt l_env = function
  | StmtAssign (lid, exp) -> " s " ^ " = " ^ why_of_exp l_env true exp 
  | StmtAssert (exp)      -> "  ( " ^ why_of_exp l_env false exp ^ " ) (* assert *) "
 *)

(* 
let pred_of_stmts id l_env stmtl = 
  String.concat ("predicate_" ^ nl) (List.map (pred_of_st_stmt l_env) stmtl) 
*)

(* 
let pred_of_alg = function
    | FbAlg (aid, cont, l_var, stmtl) -> 
      let l_env = List.map id_of_va l_var in
        "predicate pred_alg_" ^ st_of_id aid ^ " (s : fb_state_t) : () = " ^ nl ^
        (* ref_of_vars l_var ^ *)
        ""
        (* pred_of_stmts l_env stmtl ^ nl
          *)
*)

(*
let val_of_alg = function
    | FbAlg (aid, cont, l_var, stmtl) -> 
      let l_env = List.map id_of_va l_var in
        "val " ^ st_of_id aid ^ " (s : fb_state_t) : () " ^ nl ^
        "  ensures { result = " ^ nl ^ 
        "  }"
*)
                


(*
let why_of_ecc_ex_action = 
  let rec cons = function
    | []     -> "Nil"
    | e :: l -> why_of_event e  ^ " :: (" ^ cons l ^ ")" 
  in    
  
  let alg_of_actl = function
    | EcAction (Some aid, _) -> st_of_id aid ^ " s "
    | _                      -> ""
  in 
    
  function
  | None          -> ""
  | Some FbEcc (sl, _, _) ->
  
  (* let of_ecc *)
  let of_state = function
    | EcState (sid, actl) ->
      "  | " ^ why_of_sid sid ^ " -> " ^ myconcat "; " (map alg_of_actl actl) ^  cons (concat (map eid_of_act actl))   
(*      "  | " ^ why_of_sid sid ^ " -> " ^ myconcat "; " (map pred_of_actl actl) ^  cons (concat (map eid_of_act actl))   *)
  in      
  
  "(* ECC action execution *)" ^ nl ^ nl ^ 
  "val ecc_ex_action (s : fb_state_t) : list event_t " ^ nl ^ 
  "  ensures { result = " ^ 
  "  match s.ecc with " ^ nl ^
     myconcat nl (map of_state sl) ^
  "  end } " ^ nl ^ nl
 *)

(* 
let why_of_ecc_ex_trans = 
 
  (* 
  let why_of_ecc_ex_action sl = 
    let rec cons = function
      | []     -> "Nil"
      | e :: l -> why_of_event e  ^ " :: (" ^ cons l ^ ")" 
    in    
  
    let alg_of_actl = function
      | EcAction (Some aid, _) -> st_of_id aid ^ " s "
      | _                      -> ""
    in 
    
    (* let of_ecc *)
    let of_state = function
      | EcState (sid, actl) ->
        "    | " ^ why_of_sid sid ^ " -> " ^ myconcat "; " (map alg_of_actl actl) ^  cons (concat (map eid_of_act actl))   
    in      
    "    (* ECC action execution *)" ^ nl ^ nl ^ 
    "    let ecc_ex_action (s : fb_state_t) : list event_t = match s.ecc with " ^ nl ^ 
         myconcat nl (map of_state sl) ^
    "    end in" ^ nl ^ nl
   
  in  *)
  function
    
  | None               -> ""
  | Some FbEcc (sl, cl, tr) ->
  (* let of_trans *)
  let of_trans = function
    | EcTrans (s_sid, d_sid, EcGuard (_, eido, expr)) ->
      "      | (" ^ why_of_sid s_sid ^ 
      (
        match eido with 
        | None     -> ", _" 
        | Some eid -> ", Some " ^ why_of_event eid 
      )
      ^ 
      ") -> " ^
      (
        match expr with
        | IntExp 1     
        | BoolExp true -> "Some " ^ why_of_sid d_sid 
        | _            -> "if " ^ why_of_exp [] false expr ^ " then Some " ^ why_of_sid s_sid ^ " else None"
      ) 
  in  ""
  (*    
  "(* ECC transitions *)" ^ nl ^ nl ^ 
  "let rec ecc_ex (ie_opt : option event_t) (s : fb_state_t) (ls : list ecc_t) : list event_t " ^ nl ^ 
  "  variant { length ls }     (* strictly decreasing *) " ^ nl ^ 
  "  requires { mem s.ecc ls } " ^ nl ^ 
     why_of_contract [] cl ^ 
  "  = " ^ nl ^
    (* why_of_ecc_ex_action sl ^ nl ^ *)
  "    let ls' = remove s.ecc ls in" ^ nl ^
  "    let n_ecc_opt = " ^ nl ^ 
  "      match (s.ecc, ie_opt) with " ^ nl ^
         myconcat nl (map of_trans tr) ^
  "      | (_, _) -> None" ^ nl ^   
  "      end in" ^ nl ^
  "    match n_ecc_opt with " ^ nl ^ 
  "    | None -> Nil" ^ nl ^
  "    | Some n_ecc ->" ^ nl ^ 
  "      match mem n_ecc ls' with " ^ nl ^
  "      | False -> Nil (* no more transitions *)" ^ nl ^
  "      | True  ->" ^ nl ^ 
  "        s.ecc <- n_ecc;" ^ nl ^ 
  "        let oe = ecc_ex_action s in (* execute action(s) *)" ^ nl ^
  "        oe ++ (ecc_ex None s ls')" ^ nl ^ 
  "      end" ^ nl ^
  "    end" ^ nl 
  *)
*)
(*  
let why_of_ecc_ex_inline (fb_algl: fb_alg list) = 
 
  function
  | None               -> ""
  | Some FbEcc (sl, cl, tr) ->
  (* let of_trans *)
  let of_trans = function
    | EcTrans (s_sid, d_sid, EcGuard (_, eido, expr)) ->
      "      | (" ^ why_of_sid s_sid ^ 
      (
        match eido with 
        | None     -> ", _" 
        | Some eid -> ", Some " ^ why_of_event eid 
      )
      ^ 
      ") -> (* " ^ why_of_sid d_sid ^ " *) " ^ nl ^
      
      (* get the algorithms of actions *)
      let alg_of_act = function
        | EcAction (Some aid, actl) -> 
          "(* ALGORITHM " ^ st_of_id aid ^ " *)" ^ nl ^ 
          let alg = filter (fun alg -> aid = id_of_alg alg) fb_algl in
          let of_alg = function
            | FbAlg (_, _, l_var, stmtl) -> 
              let l_env = List.map id_of_va l_var in
              ref_of_vars l_var ^ 
              why_of_stmts l_env stmtl ^ ";" 
          in    
          String.concat nl (map of_alg alg)
        | _                      -> ""
      in 
      
      (* get the destination state *)
      let ds = filter (fun st -> d_sid = sid_of_st st) sl in
      let of_ds = function
        | EcState (_, actl) -> (myconcat nl (map alg_of_act actl), concat (map eid_of_act actl))
      in
      let dsl = map of_ds ds in
      let algs = map fst dsl in
      let oel = concat (map snd dsl) in
      myconcat nl algs ^
         
      (
        match expr with
        | IntExp 1     
        | BoolExp true -> "        Some (" ^ why_of_sid d_sid ^ ", " ^ why_of_eventl oel ^ ")" 
        | _            -> "if " ^ why_of_exp [] false expr ^ " then Some " ^ why_of_sid s_sid ^ " else None"
      ) 
  in      
  "(* ECC transitions *)" ^ nl ^ nl ^ 
  "let rec ecc_ex (ie_opt : option event_t) (s : fb_state_t) (ls : list ecc_t) : list event_t " ^ nl ^ 
  "  variant { length ls }     (* strictly decreasing *) " ^ nl ^ 
  "  requires { mem s.ecc ls } " ^ nl ^ 
     why_of_contract [] cl ^ 
  "  = " ^ nl ^
  (* why_of_ecc_ex_action sl ^ nl ^ *)
  "    let ls' = remove s.ecc ls in" ^ nl ^
  "    let n_ecc_opt = " ^ nl ^ 
  "      match (s.ecc, ie_opt) with " ^ nl ^
         myconcat nl (map of_trans tr) ^
  "      | (_, _) -> None" ^ nl ^   
  "      end in" ^ nl ^
  "    match n_ecc_opt with " ^ nl ^ 
  "    | None -> Nil" ^ nl ^
  "    | Some (n_ecc, oe) ->" ^ nl ^ 
  "      match mem n_ecc ls' with " ^ nl ^
(*  "      | False -> Nil (* no more transitions *)" ^ nl ^ *)
  "      | False -> s.ecc <- n_ecc; oe (* no more transitions *)" ^ nl ^
  "      | True  -> s.ecc <- n_ecc; oe ++ (ecc_ex None s ls')" ^ nl ^ 
(*  "        let oe = ecc_ex_action s in (* execute action(s) *)" ^ nl ^ *)
  "      end" ^ nl ^
  "    end" ^ nl   
*)
                      
let why_of_fbs tl = 
  let fb = function
    | FB (fb_id, fb_if, fb_v, fb_ecc, fb_algl) -> 
      "module " ^ st_of_id fb_id ^ nl ^ nl ^
      "(* generated from FUN-4SURE (use why3 -L . [ide] st.mlw) *)" ^ nl ^ nl ^
      "use import fun4sure.Fun4Sure" ^ nl ^ nl ^
      why_of_fb fb_if fb_v fb_ecc fb_algl ^ 
      
      
    (*
      (
      match opt.why_il with
      | true  -> why_of_ecc_ex_inline fb_algl fb_ecc 
      | false ->
         why_of_ecc_ex_action fb_ecc ^ 
         why_of_ecc_ex_trans fb_ecc  
      ) ^
      *)
      "end"
  in
  myconcat nl (List.map fb tl) 

    
